p:FinProbSpace, C:p-open(p). measure(C) = 1   

latex

Definitions

measure(C) = 1, x:A. B(x), tt, r - s, (r/s), x,y. t(x;y), , qeq(r;s), EquivRel(T;x,y.E(x;y)), if b then t else f fi , x,y:A//B(x;y), A  B, , , E(n;F), p-open(p), Top, , RandomVariable(p;n), x.A(x), FinProbSpace, Type, f(a), <a, b>, suptype(S; T), , S  T, Outcome, type List, x:A  B(x), s = t, a  j < b. E(j), l[i], xL. P(x), x. t(x), r  s, #$n, (x  l), , x:A. B(x), t  T, x:AB(x), Void, {i..j}, {x:A| B(x)} , , i  j < k, A  B, P & Q, A, False, P  Q, a < b, ||as||

Lemmas

l member wf, int inc rationals, qle wf, l all wf2, int seg wf, select wf, length wf1, qsum wf, rationals wf, p-outcome wf, le wf, nat wf, length wf nat, expectation wf, qeq wf2, quotient wf, int-rational, nat plus inc int nzero, int nzero-rational, qdiv wf, qsub wf, btrue wf, bool wf, int nzero wf, b-union wf, nat plus wf